poss:(ES{i}Prop{i'}), e1, e2:possible-event{i:l}(poss). poss-le{i:l}(e1; e2)  Prop{i'} 

latex

Definitions	Type, Prop, t  T, ES, x:AB(x), f(a), x:A. B(x), E, x:AB(x), 1of(t), True, T, S  T, x.A(x), EqDecider(T), Unit, left+right, IdLnk, Id, EOrderAxioms(E; pred?; info), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), type List, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val), AtomFree(T;x), P & Q, Top, x. t(x), 2of(t), A/x,y. B(x;y), e  e' , s = t, A & B, e1  e2, PossibleEvent(poss)
Lemmas	es-le wf, pi1 wf, pi2 wf, squash wf, true wf, es-E wf, event system wf